COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\CSCOTT INDUCTION IN SET THEORY
C00005 ENDMK
C⊗;
\CSCOTT INDUCTION IN SET THEORY

\Cby John McCarthy


\J	Scott's (1969) form of induction is the most powerful now available
in mathematical theory of computation, and its incorportation by
Milner (1972) in the LCF proof checker yields a system proving many
assertions about programs.  However, the Scott and Milner systems achieve
their simplicity by making sure that the only objects in the theory are
monotonic and continuous and the formulas all admit Scott induction.
This prevents sentences in the theory from being negated and thus prevents
the full apparatus of predicate calculus.  Unfortunately, this apparatus and
the apparatus of set theory is necessary in order to deal flexibly with
wide classes of mathematical entities including many that arise in programming.
Putting the Scott system in set theory requires a complete restructuring of
the theory, and the first results in this direction were obtained by
Igarashi (1972), but his results were rather informal and did not solve the
problem of how to handle λ-expressions.  This memorandum sketches a solution
to this.

	1. We will work within an axiomatization of set theory in first order
logic.  The logic will contain functions as well as predicates, and the
set theory will contain functions as individuals.  The set theory will be of
the Zermelo-Frankel type and will contain a strong axiom schema of reducibility
like that in Cohen (1965).  We hope that the formal machinery will provide
in a smooth way for all the tricks Cohen does informally.